Nuprl Lemma : listp_wf
11,40
postcript
pdf
A
:Type. listp(
A
)
Type
latex
Definitions
listp(
A
)
,
t
T
,
x
:
A
.
B
(
x
)
,
prop{i:l}
Lemmas
length
wf1
,
lt
int
wf
,
assert
wf
origin
A:Type. listp(A) 
Type A:Type. listp(A) Type Tx:A. B(x)